\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $B$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]$f$:(\=$\cap$$z$:$\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq$r ${\it ds}$($x$)?Top.\{\=$e$:E$\mid$ \+\+
\\[0ex]loc($e$) = source($l$) $\in$ Id
\\[0ex]\& (valtype($e$) $\subseteq$r $A$)\} 
\-\\[0ex]$\rightarrow$(?$B$)).
\-\-\\[0ex]state ${\it ds}$$k$:$A$ sends [${\it tg}$, $e$.$f$($e$):$B$] on $l$ $\in$ $\mathbb{P}$
\end{tabbing}